\begin{tabbing}
$\forall$${\it the\_w}$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ (\=$\forall$$e$:E.\+
\\[0ex]isrcv(kind($e$))
\\[0ex]$\Rightarrow$ \=sends(lnk(kind($e$));sender($e$))[index($e$)]\+
\\[0ex]$=$
\\[0ex]msg(lnk(kind($e$));tag(kind($e$));val($e$))
\\[0ex]$\in$ Msg(${\it the\_w}$.M))
\-\-
\end{tabbing}